Definitions

Id, sq_type(T), x:A. B(x), P  Q, t  T, prop{i:l}